Premise (Indicated by “P”) - If "P" is a premise of the argument being derived, then "P" may be written as a new line in the derivation.

Box and Cancel (“DP”)  If the formula indicated by "show" is available below that show line, and there is no other uncancelled "show" between that show line and that formula, then that "show" may be cancelled, and a box may be drawn around that formula and any other lines there may be between it and it's show line. If the relevant show line is line #1, then the derivation is finished.

Conjunction (“CJ”)  If "P" and "Q" are both available lines, they can be joined together by putting a " ^ " between them to make a new sentence "P ^ Q" which may be written as a new line in the derivation.

Simplification (“S”) If "P ^ Q" is an available line, then either "P" or "Q" may be written as a new line in the derivation.

Assumption for Indirect Proof (“AIP”) Whenever you write a show line for any formula, you can write the exact negation of that formula, provided that it is the very next thing you write.

Indirect Proof (“IP”) If any formula and its negation are both available without an uncancelled "show" between them, then the closest "show" that is above them both may be cancelled, and a box may be drawn around the closest one and any other lines there may be between it and that show line. If the relevant show line is line #1, then the derivation is successfully finished. (“Put IP by the "show”)

Double Negation ( "NN”)   You can add two negations to any available formula "Q" to make "~ ~Q," when any available formula begins with two negations that modify the whole rest of that formula, "~ ~P," you can remove those two negations to make "P" and 

Addition (“AD”)   If "P" is an available line, any formula "Q" (“available or not”) can be added to P by putting a wedge "v" between them to make a new sentence "P v Q" or "Q v P" which may be written as a new line in the derivation.

Disjunctive Syllogism (“DS”)  If "P v Q" and "~Q" are both available lines, then "P" may be written as a new line.
If "P v Q" and "~P" are both available lines, then "Q" may be written as a new line.

Commutativity (“CM”) If "P ^ Q" is an available line, then "Q ^ P" may be written as a new line.
If "P v Q" is an available line, then "Q v P" may be written as a new line.

Modus Ponens (“MP”) If "P É Q" and "P" are both available lines, then "Q" may be written as a new line in the derivation.

Modus Tollens (“MT”) If "P É Q" and "~Q" are both available lines, then "~P" may be written as a new line in the derivation.

Conditional Proof (“CP”)  
A. IF, and ONLY IF, you first write a show line of "Show P É Q" you may write "P" as the next line, justifying it by "ACP" 
B. IF, and ONLY IF, you subsequently produce "Q" as an available line, and there is no other uncancelled "show" between that show line and that "Q", then that "show" may be cancelled, and a box may be drawn around that formula and any other lines there may be between it and it's show line. If the relevant show line is line #1, then the derivation is successfully finished. (“Put "CP" by the show.”) 

Repetition (“R”) If "P" appears as an available line, then "P" may be written as a new line.

Pack Biconditional (“PB”) If Q É P and P É Q are both available, then P  Q may be written as a new line in the derivation.

Unpack Biconditional (“UB”) If P  Q is an available line, then Q É P or P É Q may be written as a new line in the derivation.

Theorem (“Thm <number of theorem>“) If T is a theorem containing sentence letters such as "P," "Q," "R" etc, an "instance" of that theorem may be written in as a new line in which every "P" is replaced by exactly the same sentence, and so on. 

De Morgan's Laws (“DML”) Comes in four little rules. 
1. If "~(“R ^ S”)" is an available line, then "~R v ~S" may be written as a new line in the derivation, and 
2. If "~(“R v S”)" is an available line, then "~R ^ ~S" may be written as a new line in the derivation, and 
3. If "~R v ~S" is an available line, then "~(“R ^ S”)" may be written as a new line in the derivation, and 
4. If "~R ^ ~S" is an available line, then "~(“R v S”)" may be written as a new line in the derivation

Theorem 1. P É P					Theorem 7. (Q É P) É (~Q v P)
Theorem 2. P É (Q É P)				Theorem 8. (~Q v P) É (Q É P)
Theorem 3. [(P ^ Q) É R]  [P É (Q É R)]		Theorem 9. (Q É P) É ~(Q ^ ~P)
Theorem 4. [(P ^ Q) É R]  [Q É (P É R)]		Theorem 10. ~(Q ^ ~P) É (Q É P)
Theorem 5. ~(P ^ Q)  (~P v ~Q)
Theorem 6. ~(P v Q)  (~Q ^ ~P)